Nuprl Lemma : K-sem_wf
0,22
postcript
pdf
Pgm
,
Sem
:Type,
S
:(
Pgm
Sem
),
equiv
:(
Sem
Sem
Prop). K-sem(
S
;
equiv
)
(
Sem
Pgm
)
Sem
Prop
latex
Definitions
t
T
,
Prop
,
x
:
A
.
B
(
x
)
,
K-sem(
S
;
equiv
)
origin
Pgm, Sem:Type, S:(Pgm
Sem), equiv:(SemSemProp). K-sem(S;equiv) 
(SemPgm)SemProp Pgm, Sem:Type, S:(PgmSem), equiv:(SemSemProp). K-sem(S;equiv) (SemPgm)SemProp Tx:A. B(x)